package kodkod.analysis.visitor;

import java.util.ArrayList;
import kodkod.ast.*;

public class QuantifierType extends IncomingEdges {
	
	public ArrayList<LeafExpression> allQuantified = new ArrayList<LeafExpression>();
	public ArrayList<LeafExpression> existQuantified = new ArrayList<LeafExpression>();

	public QuantifierType(Formula formula) {
		this.visit(formula);
	}
	
	@Override
	public void visit(QuantifiedFormula quantFormula) {
		super.visit(quantFormula);
		for (Decl decl : quantFormula.decls()) {
			if (quantFormula.quantifier().toString().equals("all")) {
				allQuantified.add(decl.variable());
				if (decl.expression() instanceof LeafExpression) {
					allQuantified.add((LeafExpression)decl.expression());
				}
			} else if (quantFormula.quantifier().toString().equals("some")) {
				existQuantified.add(decl.variable());
				if (decl.expression() instanceof LeafExpression) {
					existQuantified.add((LeafExpression)decl.expression());
				}
			}
		}
	}
}
